/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package chameleon.model;

import chameleon.model.formula.Formula;
import java.util.Hashtable;

/**
 * This class represent a Transition on an automaton.
 *
 * The NuSmv format for a node is  : (src & label) -> next(target)
 *
 * @author simon
 */
public class NodeTrans {

    private Formula src_;
    private Formula target_;
    private Formula label_;

    public NodeTrans(Formula src, Formula target, Formula label){
        src_ = src;
        target_ = target;
        if (!label.isTrue())
            label_ = label;
        else
            label_=null;
    }

    public NodeTrans(Formula src, Formula target){
        src_ = src;
        target_ = target;
        label_ = null;
    }

    private NodeTrans(NodeTrans node){
        src_ = node.getSrc().clone();
        target_ = node.getTarget().clone();
        if (node.getLabel() != null)
            label_ = node.getLabel().clone();
        else
            label_ = null;
    }


    public Formula getSrc(){
        return src_;
    }

    public Formula getTarget(){
        return target_;
    }

    public Formula getLabel(){
        return label_;
    }

    @Override
    public NodeTrans clone(){
        return new NodeTrans(this);
    }

    @Override
    public String toString(){
        if (label_ != null)
            return src_.toString()+" & "+label_.toString()+" -> next("+
                target_.toString()+")";
        else
            return src_.toString()+" -> next("+
                target_.toString()+")";
    }

    /**
     * This class convert the representation of the transition to an other format
     * define in convertTable.
     *
     * key : old format , value : new format
     *
     * @param convertTable
     */

    public void convert(Hashtable convertTable){
        src_.convert(convertTable);
        target_.convert(convertTable);
        label_.convert(convertTable);
    }

}
